Nuprl Definition : igrp 13,42
IGroup == {g:IMonoid| Inverse(|g|;*;e;~)}  
latex

clarification:

IGroup{i} == {g:IMonoid{i}| Inverse(|g|;*g;eg;~g)}  
latex

Upgroups 1
Wellformedness Lemmasigrp wf
DefinitionsIMonoid, Inverse(T;op;id;inv), |g|, *, e, ~

origin